\begin{tabbing}
es{-}update{-}iff(${\it es}$;$i$;$x$;${\it ds}$;$e$.$P$($e$);$s$.$f$($s$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. vartype($i$;$x$) $\subseteq$r ${\it ds}$($x$)?Top)\+
\\[0ex]c$\wedge$ \=$\forall$$e$@$i$.\+
\\[0ex]($P$($e$) $\Rightarrow$ (($x$ after $e$) = $f$((state when $e$))))
\\[0ex]\& (($\neg$$P$($e$)) $\Rightarrow$ (($x$ after $e$) = ($x$ when $e$)))
\-\-
\end{tabbing}